onceR{$a:ut2, $done:ut2}
onceR(i)
== ([@i precondition for "$a"(v:Unit):
== ([@i s,v. s."$done" = false State("$done" : ) v
== (; @i "$done" initially false:
== (; @i effect locl("$a")(v:Unit)  "$done" := s,v. true State("$done" : ) v 
== (; @i only events in [locl("$a")] change "$done":]) 

latex

---

clarification:

onceR{$a:ut2, $done:ut2}
onceR(i)
== ([@i precondition for "$a"(v:Unit):
== ([@i s,v. s."$done" = false   State("$done" : ) v
== (; @i "$done" initially false:
== (; @i effect locl("$a")(v:Unit)  "$done" := s,v. true State("$done" : ) v 
== (/ @i only events in locl("$a").nil change "$done":.nil]) 

latex

Definitions

(L), @loc precondition for a(v:T):P State(ds) v, s = t, s.x, @loc x initially v:T, false, @loc effect knd(v:T)  x := f State(ds) v , x : v, Unit, x.A(x), true, @loc only events in L change x:T, , car.cdr, locl(a), "$x", nil